es:ES, T:Type, c:T, i, x:Id.
@i x initially c:T  {vartype(i;x)  T & e@i. first(e)  (x when e) = c  T} 

latex

Definitions	ES, t  T, Type, Id, x:A. B(x), x initially@i , x:AB(x), vartype(i;x), s = t, Prop, A & B, x:AB(x), x when e, <a,b>, E, loc(e), first(e), b, P  Q, {T}, e@i. P(e), @i x initially v:T, SQType(T), s ~ t, Atom$n
Lemmas	es-when-first, Id sq, assert wf, es-first wf, es-loc wf, es-E wf, es-vartype wf, es-initially wf, Id wf, event system wf